Yesterday, we wrapped up first-order logic.

In particular, we talked about machine-oriented

calcali for theorem proving in first-order logic,

proving new knowledge from old knowledge,

knowledge that is entailed by the current world state

in an expressive logic.

Since we have an expressive logic,

we should not be shocked that

the inference procedures are getting

a little bit more difficult.

In this particular case,

we looked at two inference procedures.

One is first-order tableaus,

where the central innovation is that instead of

closing complementary literals, namely,

a false and a true together must be a contradiction.

We relaxed that by saying,

do we find in the tableau two literals that we can

make contradictory via a substitution?

That shifts some of the problem,

namely the problem of choosing

the right terms in the universal rule up to

a later place where we hopefully have more information.

By and large, in practice,

this works very well, as we've seen in the example.

The problem is that we want to solve,

is can we find a substitution that makes

two terms in first-order logic equal?

Can we do so with the least amount commitment possible?

It turns out that there's an algorithm for

that called unification.

Unification, the algorithm is one that lends

itself to being written down as a calculus.

If that is the case,

we can use the calculus to make

certain properties of the algorithm,

make them explicit, and prove things about them.

So what you've seen yesterday in a sequence of Lemata was,

we actually proved properties of this algorithm,

something we haven't done before.

Normally, I show you a little bit of pseudo code,

wave my hands vigorously and say,

oh yeah, obviously it does what we want.

Then you probably think a bit and say,

yeah, it probably doesn't what we want.

Normally, we would go about,

if we had an algorithm like that,

implement it, test it,

and see whether it does the expected thing.

Does it find Rome when you're looking for